The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

Rewrite Strategy: FULL

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

S is empty.
Rewrite Strategy: FULL

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
inc(s(x)) →⁺ s(inc(x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x / s(x)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)